package model.logic;

import model.logic.operand.Operand;
import model.logic.operand.Variable;
import model.logic.operand.ZeroConstant;
import model.logic.operator.Operator;

public class Proposition {
	
	private final boolean negated;
	private final Operator operator;
	private final Variable x;
	private final Operand y;
	
	public Proposition(boolean negated, Operator operator, Variable x, Variable y) {
		this.negated = negated;
		this.operator = operator;
		this.x = x;
		this.y = y;
	}
	
	public Proposition(boolean negated, Operator operator, Variable x) {
		this.negated = negated;
		this.operator = operator;
		this.x = x;
		this.y = ZeroConstant.getInstance();
	}
	
	public boolean derives(Proposition p) {
		return this.equals(p);
	}
	
	
	
	@Override
	public int hashCode() {
		final int prime = 31;
		final int truePrime = 1231;
		final int falsePrime = 1237;
		int result = 1;
		result = prime * result + (this.negated ? truePrime : falsePrime);
		result = prime * result
				+ ((this.operator == null) ? 0 : this.operator.hashCode());
		result = prime * result + ((this.x == null) ? 0 : this.x.hashCode());
		result = prime * result + ((this.y == null) ? 0 : this.y.hashCode());
		return result;
	}

	@Override
	public boolean equals(Object obj) {
		return obj instanceof Proposition ? ((Proposition) obj).equals(this) : false;
	}
	
	/**
	 * Checks whether two <tt>Propositions</tt> are equal or not. <br>
	 * 
	 * @param obj Proposition to be checked 
	 * @return true <=> 
	 */
	private boolean equals(Proposition obj) { 
		if (this.isNegated() != obj.isNegated()) {
			return false;
		}
		if (!this.getOperator().equals(obj.getOperator())) {
			return false;
		}
		
		if (this.getX().equals(obj.getX()) && this.getY().equals(obj.getY())) {
			return true;
		}
		
		if (this.getOperator().isSymmetric() && this.getX().equals(obj.getY()) 
				&& this.getY().equals(obj.getX())) {
			return true;
		}
		return false;
	}
	
	public boolean isNegated() {
		return this.negated;
	}

	public Operator getOperator() {
		return this.operator;
	}

	public Variable getX() {
		return this.x;
	}

	public Operand getY() {
		return this.y;
	}
}
